0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 5 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 14 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
pA_in_ga(T4, T4) → pA_out_ga(T4, T4)
pA_in_ga(f(T22), g(T9)) → U1_ga(T22, T9, pA_in_gg(T22, g(T9)))
pA_in_gg(T4, T4) → pA_out_gg(T4, T4)
pA_in_gg(f(T22), g(T9)) → U1_gg(T22, T9, pA_in_gg(T22, g(T9)))
pA_in_gg(f(T45), g(T32)) → U2_gg(T45, T32, pA_in_gg(T45, g(T32)))
U2_gg(T45, T32, pA_out_gg(T45, g(T32))) → pA_out_gg(f(T45), g(T32))
U1_gg(T22, T9, pA_out_gg(T22, g(T9))) → pA_out_gg(f(T22), g(T9))
U1_ga(T22, T9, pA_out_gg(T22, g(T9))) → pA_out_ga(f(T22), g(T9))
pA_in_ga(f(T45), g(T32)) → U2_ga(T45, T32, pA_in_gg(T45, g(T32)))
U2_ga(T45, T32, pA_out_gg(T45, g(T32))) → pA_out_ga(f(T45), g(T32))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
pA_in_ga(T4, T4) → pA_out_ga(T4, T4)
pA_in_ga(f(T22), g(T9)) → U1_ga(T22, T9, pA_in_gg(T22, g(T9)))
pA_in_gg(T4, T4) → pA_out_gg(T4, T4)
pA_in_gg(f(T22), g(T9)) → U1_gg(T22, T9, pA_in_gg(T22, g(T9)))
pA_in_gg(f(T45), g(T32)) → U2_gg(T45, T32, pA_in_gg(T45, g(T32)))
U2_gg(T45, T32, pA_out_gg(T45, g(T32))) → pA_out_gg(f(T45), g(T32))
U1_gg(T22, T9, pA_out_gg(T22, g(T9))) → pA_out_gg(f(T22), g(T9))
U1_ga(T22, T9, pA_out_gg(T22, g(T9))) → pA_out_ga(f(T22), g(T9))
pA_in_ga(f(T45), g(T32)) → U2_ga(T45, T32, pA_in_gg(T45, g(T32)))
U2_ga(T45, T32, pA_out_gg(T45, g(T32))) → pA_out_ga(f(T45), g(T32))
PA_IN_GA(f(T22), g(T9)) → U1_GA(T22, T9, pA_in_gg(T22, g(T9)))
PA_IN_GA(f(T22), g(T9)) → PA_IN_GG(T22, g(T9))
PA_IN_GG(f(T22), g(T9)) → U1_GG(T22, T9, pA_in_gg(T22, g(T9)))
PA_IN_GG(f(T22), g(T9)) → PA_IN_GG(T22, g(T9))
PA_IN_GG(f(T45), g(T32)) → U2_GG(T45, T32, pA_in_gg(T45, g(T32)))
PA_IN_GA(f(T45), g(T32)) → U2_GA(T45, T32, pA_in_gg(T45, g(T32)))
pA_in_ga(T4, T4) → pA_out_ga(T4, T4)
pA_in_ga(f(T22), g(T9)) → U1_ga(T22, T9, pA_in_gg(T22, g(T9)))
pA_in_gg(T4, T4) → pA_out_gg(T4, T4)
pA_in_gg(f(T22), g(T9)) → U1_gg(T22, T9, pA_in_gg(T22, g(T9)))
pA_in_gg(f(T45), g(T32)) → U2_gg(T45, T32, pA_in_gg(T45, g(T32)))
U2_gg(T45, T32, pA_out_gg(T45, g(T32))) → pA_out_gg(f(T45), g(T32))
U1_gg(T22, T9, pA_out_gg(T22, g(T9))) → pA_out_gg(f(T22), g(T9))
U1_ga(T22, T9, pA_out_gg(T22, g(T9))) → pA_out_ga(f(T22), g(T9))
pA_in_ga(f(T45), g(T32)) → U2_ga(T45, T32, pA_in_gg(T45, g(T32)))
U2_ga(T45, T32, pA_out_gg(T45, g(T32))) → pA_out_ga(f(T45), g(T32))
PA_IN_GA(f(T22), g(T9)) → U1_GA(T22, T9, pA_in_gg(T22, g(T9)))
PA_IN_GA(f(T22), g(T9)) → PA_IN_GG(T22, g(T9))
PA_IN_GG(f(T22), g(T9)) → U1_GG(T22, T9, pA_in_gg(T22, g(T9)))
PA_IN_GG(f(T22), g(T9)) → PA_IN_GG(T22, g(T9))
PA_IN_GG(f(T45), g(T32)) → U2_GG(T45, T32, pA_in_gg(T45, g(T32)))
PA_IN_GA(f(T45), g(T32)) → U2_GA(T45, T32, pA_in_gg(T45, g(T32)))
pA_in_ga(T4, T4) → pA_out_ga(T4, T4)
pA_in_ga(f(T22), g(T9)) → U1_ga(T22, T9, pA_in_gg(T22, g(T9)))
pA_in_gg(T4, T4) → pA_out_gg(T4, T4)
pA_in_gg(f(T22), g(T9)) → U1_gg(T22, T9, pA_in_gg(T22, g(T9)))
pA_in_gg(f(T45), g(T32)) → U2_gg(T45, T32, pA_in_gg(T45, g(T32)))
U2_gg(T45, T32, pA_out_gg(T45, g(T32))) → pA_out_gg(f(T45), g(T32))
U1_gg(T22, T9, pA_out_gg(T22, g(T9))) → pA_out_gg(f(T22), g(T9))
U1_ga(T22, T9, pA_out_gg(T22, g(T9))) → pA_out_ga(f(T22), g(T9))
pA_in_ga(f(T45), g(T32)) → U2_ga(T45, T32, pA_in_gg(T45, g(T32)))
U2_ga(T45, T32, pA_out_gg(T45, g(T32))) → pA_out_ga(f(T45), g(T32))
PA_IN_GG(f(T22), g(T9)) → PA_IN_GG(T22, g(T9))
pA_in_ga(T4, T4) → pA_out_ga(T4, T4)
pA_in_ga(f(T22), g(T9)) → U1_ga(T22, T9, pA_in_gg(T22, g(T9)))
pA_in_gg(T4, T4) → pA_out_gg(T4, T4)
pA_in_gg(f(T22), g(T9)) → U1_gg(T22, T9, pA_in_gg(T22, g(T9)))
pA_in_gg(f(T45), g(T32)) → U2_gg(T45, T32, pA_in_gg(T45, g(T32)))
U2_gg(T45, T32, pA_out_gg(T45, g(T32))) → pA_out_gg(f(T45), g(T32))
U1_gg(T22, T9, pA_out_gg(T22, g(T9))) → pA_out_gg(f(T22), g(T9))
U1_ga(T22, T9, pA_out_gg(T22, g(T9))) → pA_out_ga(f(T22), g(T9))
pA_in_ga(f(T45), g(T32)) → U2_ga(T45, T32, pA_in_gg(T45, g(T32)))
U2_ga(T45, T32, pA_out_gg(T45, g(T32))) → pA_out_ga(f(T45), g(T32))
PA_IN_GG(f(T22), g(T9)) → PA_IN_GG(T22, g(T9))
PA_IN_GG(f(T22), g) → PA_IN_GG(T22, g)
From the DPs we obtained the following set of size-change graphs: